Пронумеруем типы и их значения

Конгруэнтная функция encode, которая для любого индуктивного типа возвращает
натуральное число. Обратная тотальная функция выбирает сигнатуру индуктивного
типа и указатель на стрим населяемых значений.

encode (X: Type) -> Nat
decode (X: Nat) -> (Sig: Type, Values: Stream Sig)

Еще это можно назвать — глобальное управление контекстами. Функция decode —
может состоять из генератора Values: Nat -> Sig, который аллоцирует в
виртуальной машине уникальный инстанс типа Sig по заданному Nat. Таким образом
каждая возможная переменная в пространстве типов и термов на всех уровнях может
индексироваться тройков Nat значений (Nat,Nat,Nat) — индекс вселенной, индекс
типа, и индекс инстанса.

Конструирование термов в зависимом тайпчекере:

0 — UNIT      =
1 — NORM      = Nat      // normalisation
2 — SUBST     = Nat      // substitution
3 — STAR      = Nat      // universe
4 — REC       = Nat      // Cons: A -> List A -> List A
5 — VAR       = Nat Nat  // Nat, Bool, List A, Vec Nat A
6 — OR        = Nat Nat  // data
7 — AND       = Nat Nat  // record
8 — EQ        = Nat Nat  // definition
9 — PI        = Nat Nat Nat
A — FUN       = Nat Nat Nat
B — TYPECHECK = Nat

Пример:

encode "List A = Nil: List A | Cons: A -> List A -> List A"

0 — UNIT        // "A"
1 — UNIT        // "Nil"
2 — UNIT        // "Cons"
3 — UNIT        // "List"
4 — VAR 0 _     // A
5 — VAR 3 4     // List A
6 — REC 5       // Rec List A
7 — AND 4 6     // (A, Rec List A)
8 — VAR 2 7     // Cons: A -> List A
9 — VAR 1 _     // Nil:
A — OR 9 8      // Nil: | Cons:
B — EQ 5 A      // List A = Nil: List A | Cons: A -> List A -> List A


— основные конструкторы, которые индексируют (кроме Unit), некоторую переменную
в таблице имен (индексы де Брейна), значение которой составляет тройка, таким
образом словарь контекстов — List (Nat, (Nat, Nat, Nat)) — закодирован списком
пар.

Для сравнения, List A в формате Lean:

1 — NS 0 u
2 — NS 0 list
3 — NS 0 α
1 — UP 1
0 — ES 1
1 — EP BD 3 0 0
4 — NS 2 nil
2 — EC 2 1
3 — EV 0
4 — EA 2 3
5 — EP BD 3 0 4
5 — NS 2 cons
6 — NS 0 a
6 — EV 1
7 — EA 2 6
8 — EV 2
9 — EA 2 8
A — EP BD 6 7 9
B — EP BD 6 3 10
C — EP BI 3 0 11
D — IND 1 2 1 2 4 5 5 12 1